10.11.4 Algebraic Properties of Rewrite Rules

The rewrite mechanism understands the algebraic properties of functions like ‘+’ and ‘*’. In particular, pattern matching takes the associativity and commutativity of the following functions into account:

+ - *  = !=  && ||  and or xor  vint vunion vxor  gcd lcm  max min  beta

For example, the rewrite rule:

a x + b x  :=  (a + b) x

will match formulas of the form,

a x + b x,  x a + x b,  a x + x b,  x a + b x

Rewrites also understand the relationship between the ‘+’ and ‘-’ operators. The above rewrite rule will also match the formulas,

a x - b x,  x a - x b,  a x - x b,  x a - b x

by matching ‘b’ in the pattern to ‘-b’ from the formula.

Applied to a sum of many terms like ‘r + a x + s + b x + t’, this pattern will check all pairs of terms for possible matches. The rewrite will take whichever suitable pair it discovers first.

In general, a pattern using an associative operator like ‘a + b’ will try 2 n different ways to match a sum of n terms like ‘x + y + z - w’. First, ‘a’ is matched against each of ‘x’, ‘y’, ‘z’, and ‘-w’ in turn, with ‘b’ being matched to the remainders ‘y + z - w’, ‘x + z - w’, etc. If none of these succeed, then ‘b’ is matched against each of the four terms with ‘a’ matching the remainder. Half-and-half matches, like ‘(x + y) + (z - w)’, are not tried.

Note that ‘*’ is not commutative when applied to matrices, but rewrite rules pretend that it is. If you type m v to enable Matrix mode (see Matrix Mode), rewrite rules will match ‘*’ literally, ignoring its usual commutativity property. (In the current implementation, the associativity also vanishes—it is as if the pattern had been enclosed in a plain marker; see below.) If you are applying rewrites to formulas with matrices, it’s best to enable Matrix mode first to prevent algebraically incorrect rewrites from occurring.

The pattern ‘-x’ will actually match any expression. For example, the rule

f(-x)  :=  -f(x)

will rewrite ‘f(a)’ to ‘-f(-a)’. To avoid this, either use a plain marker as described below, or add a ‘negative(x)’ condition. The negative function is true if its argument “looks” negative, for example, because it is a negative number or because it is a formula like ‘-x’. The new rule using this condition is:

f(x)  :=  -f(-x)  :: negative(x)    or, equivalently,
f(-x)  :=  -f(x)  :: negative(-x)

In the same way, the pattern ‘x - y’ will match the sum ‘a + b’ by matching ‘y’ to ‘-b’.

The pattern ‘a b’ will also match the formula ‘x/y’ if ‘y’ is a number. Thus the rule ‘a x + b x := (a+b) x’ will also convert ‘a x + x / 2’ to ‘(a + 0.5) x’ (or ‘(a + 1:2) x’, depending on the current fraction mode).

Calc will not take other liberties with ‘*’, ‘/’, and ‘^’. For example, the pattern ‘f(a b)’ will not match ‘f(x^2)’, and ‘f(a + b)’ will not match ‘f(2 x)’, even though conceivably these patterns could match with ‘a = b = x’. Nor will ‘f(a b)’ match ‘f(x / y)’ if ‘y’ is not a constant, even though it could be considered to match with ‘a = x’ and ‘b = 1/y’. The reasons are partly for efficiency, and partly because while few mathematical operations are substantively different for addition and subtraction, often it is preferable to treat the cases of multiplication, division, and integer powers separately.

Even more subtle is the rule set

[ f(a) + f(b) := f(a + b),  -f(a) := f(-a) ]

attempting to match ‘f(x) - f(y)’. You might think that Calc will view this subtraction as ‘f(x) + (-f(y))’ and then apply the above two rules in turn, but actually this will not work because Calc only does this when considering rules for ‘+’ (like the first rule in this set). So it will see first that ‘f(x) + (-f(y))’ does not match ‘f(a) + f(b)’ for any assignments of the meta-variables, and then it will see that ‘f(x) - f(y)’ does not match ‘-f(a)’ for any assignment of ‘a’. Because Calc tries only one rule at a time, it will not be able to rewrite ‘f(x) - f(y)’ with this rule set. An explicit ‘f(a) - f(b)’ rule will have to be added.

Another thing patterns will not do is break up complex numbers. The pattern ‘myconj(a + b i) := a - b i’ will work for formulas involving the special constant ‘i’ (such as ‘3 - 4 i’), but it will not match actual complex numbers like ‘(3, -4)’. A version of the above rule for complex numbers would be

myconj(a)  :=  re(a) - im(a) (0,1)  :: im(a) != 0

(Because the re and im functions understand the properties of the special constant ‘i’, this rule will also work for ‘3 - 4 i’. In fact, this particular rule would probably be better without the ‘im(a) != 0’ condition, since if ‘im(a) = 0’ the righthand side of the rule will still give the correct answer for the conjugate of a real number.)

It is also possible to specify optional arguments in patterns. The rule

opt(a) x + opt(b) (x^opt(c) + opt(d))  :=  f(a, b, c, d)

will match the formula

5 (x^2 - 4) + 3 x

in a fairly straightforward manner, but it will also match reduced formulas like

x + x^2,    2(x + 1) - x,    x + x

producing, respectively,

f(1, 1, 2, 0),   f(-1, 2, 1, 1),   f(1, 1, 1, 0)

(The latter two formulas can be entered only if default simplifications have been turned off with m O.)

The default value for a term of a sum is zero. The default value for a part of a product, for a power, or for the denominator of a quotient, is one. Also, ‘-x’ matches the pattern ‘opt(a) b’ with ‘a = -1’.

In particular, the distributive-law rule can be refined to

opt(a) x + opt(b) x  :=  (a + b) x

so that it will convert, e.g., ‘a x - x’, to ‘(a - 1) x’.

The pattern ‘opt(a) + opt(b) x’ matches almost any formulas which are linear in ‘x’. You can also use the lin and islin functions with rewrite conditions to test for this; see Logical Operations. These functions are not as convenient to use in rewrite rules, but they recognize more kinds of formulas as linear: ‘x/z’ is considered linear with ‘b = 1/z’ by lin, but it will not match the above pattern because that pattern calls for a multiplication, not a division.

As another example, the obvious rule to replace ‘sin(x)^2 + cos(x)^2’ by 1,

sin(x)^2 + cos(x)^2  :=  1

misses many cases because the sine and cosine may both be multiplied by an equal factor. Here’s a more successful rule:

opt(a) sin(x)^2 + opt(a) cos(x)^2  :=  a

Note that this rule will not match ‘sin(x)^2 + 6 cos(x)^2’ because one ‘a’ would have “matched” 1 while the other matched 6.

Calc automatically converts a rule like

f(x-1, x)  :=  g(x)

into the form

f(temp, x)  :=  g(x)  :: temp = x-1

(where temp stands for a new, invented meta-variable that doesn’t actually have a name). This modified rule will successfully match ‘f(6, 7)’, binding ‘temp’ and ‘x’ to 6 and 7, respectively, then verifying that they differ by one even though ‘6’ does not superficially look like ‘x-1’.

However, Calc does not solve equations to interpret a rule. The following rule,

f(x-1, x+1)  :=  g(x)

will not work. That is, it will match ‘f(a - 1 + b, a + 1 + b)’ but not ‘f(6, 8)’. Calc always interprets at least one occurrence of a variable by literal matching. If the variable appears “isolated” then Calc is smart enough to use it for literal matching. But in this last example, Calc is forced to rewrite the rule to ‘f(x-1, temp) := g(x) :: temp = x+1’ where the ‘x-1’ term must correspond to an actual “something-minus-one” in the target formula.

A successful way to write this would be ‘f(x, x+2) := g(x+1)’. You could make this resemble the original form more closely by using let notation, which is described in the next section:

f(xm1, x+1)  :=  g(x)  :: let(x := xm1+1)

Calc does this rewriting or “conditionalizing” for any sub-pattern which involves only the functions in the following list, operating only on constants and meta-variables which have already been matched elsewhere in the pattern. When matching a function call, Calc is careful to match arguments which are plain variables before arguments which are calls to any of the functions below, so that a pattern like ‘f(x-1, x)’ can be conditionalized even though the isolated ‘x’ comes after the ‘x-1’.

+ - * / \ % ^  abs sign  round rounde roundu trunc floor ceil
max min  re im conj arg

You can suppress all of the special treatments described in this section by surrounding a function call with a plain marker. This marker causes the function call which is its argument to be matched literally, without regard to commutativity, associativity, negation, or conditionalization. When you use plain, the “deep structure” of the formula being matched can show through. For example,

plain(a - a b)  :=  f(a, b)

will match only literal subtractions. However, the plain marker does not affect its arguments’ arguments. In this case, commutativity and associativity is still considered while matching the ‘a b’ sub-pattern, so the whole pattern will match ‘x - y x’ as well as ‘x - x y’. We could go still further and use

plain(a - plain(a b))  :=  f(a, b)

which would do a completely strict match for the pattern.

By contrast, the quote marker means that not only the function name but also the arguments must be literally the same. The above pattern will match ‘x - x y’ but

quote(a - a b)  :=  f(a, b)

will match only the single formula ‘a - a b’. Also,

quote(a - quote(a b))  :=  f(a, b)

will match only ‘a - quote(a b)’—probably not the desired effect!

A certain amount of algebra is also done when substituting the meta-variables on the righthand side of a rule. For example, in the rule

a + f(b)  :=  f(a + b)

matching ‘f(x) - y’ would produce ‘f((-y) + x)’ if taken literally, but the rewrite mechanism will simplify the righthand side to ‘f(x - y)’ automatically. (Of course, the default simplifications would do this anyway, so this special simplification is only noticeable if you have turned the default simplifications off.) This rewriting is done only when a meta-variable expands to a “negative-looking” expression. If this simplification is not desirable, you can use a plain marker on the righthand side:

a + f(b)  :=  f(plain(a + b))

In this example, we are still allowing the pattern-matcher to use all the algebra it can muster, but the righthand side will always simplify to a literal addition like ‘f((-y) + x)’.